The present invention relates to a technology for checking the equivalence of a high-level description and a synthesis result obtained by a behavioral synthesis therewith. The present invention relates to, for example, a technology effective when applied to the support of design of a semiconductor device with a digital logic circuit integrated therein, such as a microcomputer, an SoC (system-on-chip semiconductor integrated circuit), an analog-digital mixed integrated circuit, or the like.
Upon the design of a semiconductor integrated circuit, for example, an RTL (Register-Transfer Level) description capable of logic synthesis by a behavioral synthesis system is often synthesized from a behavioral description high in abstraction level. This design method is capable of reducing the amount of description by execution of design in a behavioral level at which the abstraction level is high and greatly improving productivity of design and checking. A high-level description such as an extended language of a C language, a System C language or the like is used for the behavioral description.
In general, the behavioral synthesis system is comprised of software. As long as the software is used, it is difficult to eliminate a possibility that even with meticulous attention to detail, bugs will be included in the system itself. With the expansion of the scope of application of a behavioral synthesis, the bugs are appearing even where all checking and maintenance are conducted on the behavioral description. When, however, an erroneous RTL description is generated depending on the bugs of the behavioral synthesis system, the checking conducted on the behavioral description can be not only meaningless but also a cause that brings on rework at a post-process. The occurrence of the rework at the post-process causes increases in development period and time consuming, thus resulting in large loss. Due to such a reason, when the behavioral synthesis system is applied to actual LSI design, it is necessary to confirm the correctness of a synthesized RTL description, i.e., check that the behavioral description and the RTL description are equivalent to each other.
In terms of checking for the equivalence between the behavioral description and the RTL description, a Patent Document 1 has disclosed a method of outputting intermediate representations and correspondence relation or correlation information about variables between the intermediate representations at respective steps (pre-process step, scheduling/register binding step, arithmetic-unit binding step, and post-process step) for a behavioral synthesis, and sequentially performing equivalence checking between the intermediate representations, thereby speeding up the equivalence checking.
A method for identifying intermediate logic cones associated with each other under a given condition from a transformation history in a behavioral synthesis to thereby perform the speedup of equivalence checking has been disclosed in a Patent Document 2.
Disclosed in a Patent Document 3 is a method for extracting logic cones from both an object code obtained by compiling a behavioral level description, and an RTL description derived from the behavioral level description and assuming that a correspondence relation or correlation (pair of signals) between the behavioral level description and the RTL description is being given. That is, there has been disclosed a method for allowing the equivalence of each logic cone obtained by a symbolic simulation from the correlation information with respect to each pair of signals corresponding between the object code and the RTL description to lead to a satisfiability determination problem, thereby carrying out equivalence checking.